minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
↳ QTRS
↳ Overlay + Local Confluence
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
MINUS(x, y) → IF(gt(x, y), x, y)
MINUS(x, y) → GT(x, y)
IF(true, x, y) → MINUS(p(x), y)
IF(true, x, y) → P(x)
GE(s(x), s(y)) → GE(x, y)
GT(s(x), s(y)) → GT(x, y)
DIV(x, y) → IF1(ge(x, y), x, y)
DIV(x, y) → GE(x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(true, x, y) → GT(y, 0)
IF2(true, x, y) → DIV(minus(x, y), y)
IF2(true, x, y) → MINUS(x, y)
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS(x, y) → IF(gt(x, y), x, y)
MINUS(x, y) → GT(x, y)
IF(true, x, y) → MINUS(p(x), y)
IF(true, x, y) → P(x)
GE(s(x), s(y)) → GE(x, y)
GT(s(x), s(y)) → GT(x, y)
DIV(x, y) → IF1(ge(x, y), x, y)
DIV(x, y) → GE(x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(true, x, y) → GT(y, 0)
IF2(true, x, y) → DIV(minus(x, y), y)
IF2(true, x, y) → MINUS(x, y)
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
IF(true, x, y) → MINUS(p(x), y)
MINUS(x, y) → IF(gt(x, y), x, y)
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
IF(true, x, y) → MINUS(p(x), y)
MINUS(x, y) → IF(gt(x, y), x, y)
p(0) → 0
p(s(x)) → x
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
IF(true, x, y) → MINUS(p(x), y)
MINUS(x, y) → IF(gt(x, y), x, y)
p(0) → 0
p(s(x)) → x
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
p(0)
p(s(x0))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(true, x, y) → MINUS(p(x), y)
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
MINUS(x, y) → IF(gt(x, y), x, y)
The value of delta used in the strict ordering is 1/8.
POL(true) = 1
POL(MINUS(x1, x2)) = (1/2)x1
POL(false) = 0
POL(p(x1)) = 1/4 + (1/2)x1
POL(s(x1)) = 4 + (4)x1
POL(IF(x1, x2, x3)) = (1/4)x1 + (1/4)x2
POL(gt(x1, x2)) = x1
POL(0) = 0
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, y) → false
p(s(x)) → x
p(0) → 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
MINUS(x, y) → IF(gt(x, y), x, y)
p(0) → 0
p(s(x)) → x
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
p(0)
p(s(x0))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ UsableRulesProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF2(true, x, y) → DIV(if(gt(x, y), x, y), y)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ UsableRulesProof
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF2(true, x, y) → DIV(if(gt(x, y), x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
DIV(0, s(x0)) → IF1(false, 0, s(x0))
DIV(x0, 0) → IF1(true, x0, 0)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF2(true, x, y) → DIV(if(gt(x, y), x, y), y)
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
DIV(0, s(x0)) → IF1(false, 0, s(x0))
DIV(x0, 0) → IF1(true, x0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
IF2(true, x, y) → DIV(if(gt(x, y), x, y), y)
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, x, y) → IF2(gt(y, 0), x, y)
DIV(x0, 0) → IF1(true, x0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(true, y0, 0) → IF2(false, y0, 0)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
IF2(true, x, y) → DIV(if(gt(x, y), x, y), y)
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
DIV(x0, 0) → IF1(true, x0, 0)
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(true, y0, 0) → IF2(false, y0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, x, y) → DIV(if(gt(x, y), x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF2(true, s(x0), s(x1)) → DIV(if(gt(x0, x1), s(x0), s(x1)), s(x1))
IF2(true, 0, x0) → DIV(if(false, 0, x0), x0)
IF2(true, s(x0), 0) → DIV(if(true, s(x0), 0), 0)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, s(x0), s(x1)) → DIV(if(gt(x0, x1), s(x0), s(x1)), s(x1))
IF2(true, 0, x0) → DIV(if(false, 0, x0), x0)
IF2(true, s(x0), 0) → DIV(if(true, s(x0), 0), 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, s(x0), s(x1)) → DIV(if(gt(x0, x1), s(x0), s(x1)), s(x1))
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ MNOCProof
↳ UsableRulesProof
IF2(true, s(x0), s(x1)) → DIV(if(gt(x0, x1), s(x0), s(x1)), s(x1))
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ MNOCProof
↳ QDP
↳ UsableRulesProof
IF2(true, s(x0), s(x1)) → DIV(if(gt(x0, x1), s(x0), s(x1)), s(x1))
DIV(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
div(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ MNOCProof
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ MNOCProof
↳ QDP
IF2(true, x, y) → DIV(minus(x, y), y)
DIV(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
gt(0, y) → false
gt(s(x), 0) → true
minus(x, y) → if(gt(x, y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)